ecl-trans-reachable(ds;da;v;L;x)
== let T,ks,i,g,h,a,e = v in 
== L':event-info(ds;da) List.
== L'  L
== & ||L'||<||L||
== & & x
== & & =
== & & list_accum(x,a.a/k,zz. zz/s,v. if deq-member(KindDeq;k;ks) g(k,s,v,x) else x fi;i;L') 

latex

---

clarification:

ecl-trans-reachable(ds;da;v;L;x)
== let T,ks,i,g,h,a,e = v in 
== L':event-info(ds;da) List.
== L'  L  event-info(ds;da) List
== & ||L'||<||L||
== & & x
== & & =
== & & list_accum(x,a.a/k,zz. zz/s,v. if deq-member(KindDeq;k;ks) g(k,s,v,x) else x fi;i;L')
== & &  T 

latex

Definitions	let a,b,c,d,e,f,g = u in v(a;b;c;d;e;f;g), x:A. B(x), A & B, l1  l2, event-info(ds;da), P & Q, ||as||, list_accum(x,a.f(x;a);y;l), if b t else f fi, deq-member(eq;x;L), KindDeq
FDL editor aliases	ecl-trans-reachable